A:Type, B:(AType), f, g:a:A fp B(a), eq:EqDecider(A). f  g  a:A fp B(a) 

latex

Definitions	P  Q, False, P  Q, deq-member(eq;x;L), f(x), Unit, P  Q, P & Q, P  Q, , Prop, A, b, t  T, a:A fp B(a), x(s), f  g, 1of(t), as @ bs, filter(P;l), b, x  dom(f), EqDecider(T), (x  l), x. t(x), x:A. B(x), f(x)?z
Lemmas	fpf-trivial-subtype-top, l member wf, deq wf, fpf-dom wf, bnot wf, filter wf, append wf, pi1 wf, assert wf, not wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf-ap wf, deq-member wf, member append, assert-deq-member, not functionality wrt iff, member filter